1. Technical Field
This disclosure relates to integrated circuit (IC) design, and more particularly to formal verification of integrated circuit logic designs.
2. Description of the Related Art
In IC design, formal verification refers to a type of functional validation (verification) method that uses mathematical models of the circuits to prove a property of interest rather than relying upon simulations of individual test cases. An advantage of a formal verification is that it may be equivalent to doing an exhaustive simulation of every possible test case. Exhaustive simulation by itself is not practical for any but the most trivial of circuits because of the size of the state space.
One type of formal verification is referred to as equivalence checking. Equivalence checking is used to verify that two circuits perform the same function, where one circuit is considered to be the reference model, and the other circuit is a design model. For two circuits to be the same, each must have the same number of primary inputs (PIs) and the same number of primary outputs (POs), and there must be some way to identify corresponding inputs/outputs. Many commercial combinatorial equivalence tools may require a complete correspondence between internal sequential elements (e.g., latches or flops) of the two designs. However, because it is often necessary to modify the boundaries of modules and/or change the signal timing on the inter-module boundaries, which may break the correspondence of circuits between sequential elements, this view of equivalence may be too restrictive.
Accordingly, when the matching of sequential elements cannot be assumed, the equivalence checking is referred to as sequential equivalence checking. The sequential equivalence checking problem space may be much larger and harder than that of combinatorial equivalence checking, so application of any algorithms for proving sequential equivalence may fail due to computational complexity. If it were possible to run equivalence checking on the top-level design, nothing else would be necessary. However, because of issues with some sequential equivalence checking tools, it is often difficult to prove sequential equivalence without many iterations and trials.